l1,l2:IdLnk, d1,d2:fpf(Id; tg.Type).
((l1 = l2)  fpf-compatible(Id; x.Type; id-deq; d1; d2))
 fpf-compatible(Knd; x.Type; Kind-deq; lnk-decl(l1; d1); lnk-decl(l2; d2)) 

latex

Definitions	IdLnk, id-deq, Id, decidable(P), P  Q, sq_type(T), guard(T), fpf-compatible(A; a.B(a); eq; f; g), fpf-ap(f; eq; x), P  Q, prop{i:l}, b, fpf-dom(eq; x; f), Kind-deq, fpf(A; a.B(a)), top, x. t(x), lnk-decl(l; dt), x:A. B(x), P  Q, t  T, Knd, map(f; as), P  Q, rcv(l,tg), x:A. B(x), P  Q, deq-member(eq; x; L), (x  l), A, False
Lemmas	rcv one one, l member wf, deq-member wf, and functionality wrt iff, Knd sq, rcv wf, member map, map wf, assert-deq-member, Knd wf, lnk-decl wf, fpf-trivial-subtype-top, Kind-deq wf, fpf-dom wf, assert wf, IdLnk sq, IdLnk wf, decidable equal IdLnk, Id wf, fpf wf, id-deq wf, fpf-compatible wf